\begin{tabbing}
$\forall$${\it es}$:ES, $e$:E.
\\[0ex]($\uparrow$isrcv($e$))
\\[0ex]$\Rightarrow$ \=((index($e$) = 0)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=($\forall$${\it e'}$:E.\+
\\[0ex]($\uparrow$isrcv(${\it e'}$))
\\[0ex]$\Rightarrow$ (sender(${\it e'}$) = sender($e$) $\in$ E)
\\[0ex]$\Rightarrow$ (lnk($e$) = lnk(${\it e'}$) $\in$ IdLnk)
\\[0ex]$\Rightarrow$ $e$ $\leq$loc ${\it e'}$ ))
\-\-
\end{tabbing}